(** ** Matrix Substraction Properties *)
Require Import List.
Require Import Matrix.Mat_def.
Require Import Matrix.Mat_add.
Require Import Matrix.Mat_map.
Require Import Matrix.Mat_IO.
Require Import Matrix.list_function.

(* ################################################################# *)

(** This section separately proves various properties of matrix
    substraction, including commutation law, associativity law, left 
    sub zero matrix property and so on. *)

Section sub_lemma.

Variable A:Set.
Variable Zero:A.
Variable negative:A->A.
Variable add:A->A->A.
Variable sub:A->A->A.

(** * Matrix Substraction Commutative Law *)

(** *** dlist_sub_opp *)
(** The commutative law of the substraction of two-dimensional lists: 
    ma1 - ma2 = - (ma2 - ma1). *)
Lemma dlist_sub_opp : forall (m n:nat) (ma1 ma2:list (list A)),
  (forall a b, sub a b = negative (sub b a)) -> 
  height ma1 = m -> height ma2 = m -> 
  width ma1 n -> width ma2 n -> 
  mat_each' A sub ma1 ma2 
  = dlist_map A negative (mat_each' A sub ma2 ma1).
Proof.
  induction m.
  induction n.
  induction ma1.
  induction ma2.
  - simpl. auto.
  - simpl. intros. inversion H1.
  - induction ma2.
    + simpl. intros. auto.
    + simpl. intros. inversion H0.
  - induction ma1. induction ma2.
    + simpl. auto.
    + simpl. auto.
    + induction ma2.
      { simpl. auto. }
      { simpl. intros. inversion H0. }
  - induction n. induction ma1. induction ma2.
    + simpl. auto.
    + simpl. auto.
    + induction ma2.
      { simpl. auto. }
      { simpl. intros. f_equal. rewrite <-list_sub_opp with (negative:=negative). 
        auto. auto. apply IHm with (n:=0). auto. auto. auto. apply H2. apply H3. }
    + induction ma1. induction ma2.
      { simpl. auto. }
      { simpl. auto. }
      { induction ma2.
        { simpl. auto. }
        { simpl. intros. f_equal. rewrite <-list_sub_opp with (negative:=negative). 
          auto. auto. apply IHm with (n:=S n). auto. auto. auto. apply H2. apply H3. }
        }
Qed.
 
(** ** matrix_sub_opp *)
(** The substraction of matrices : M1 - M2 = - (M2 - M1). *)
Lemma matrix_sub_opp : forall{m n:nat} (ma1 ma2:@Mat A m n), 
  (forall a b, sub a b = negative (sub b a)) -> 
  (matrix_each A sub ma1 ma2)
  ===(matrix_map A negative (matrix_each A sub ma2 ma1)).
  
Proof.
  intros.
  induction ma1.
  induction ma2.
  unfold matrix_map.
  unfold matrix_each.
  unfold matrix_map'.
  unfold mat_each.
  simpl. unfold M_eq.
  simpl.
  apply dlist_sub_opp with (m:=m) (n:=n);auto.
Qed.

(** * Matrix Substraction Associative Law *)

(** *** dlist_sub_assoc *)
(** The associative law of the substraction of two-dimensional lists :
    dl1-dl2-dl2 = dl1-(dl2+dl3). *)
Lemma dlist_sub_assoc : forall
   (m n:nat) (dl1 dl2 dl3:list (list A)), 
  (forall a b c , sub (sub a b) c = sub a (add b c)) -> 
  height dl1 = m -> height dl2 = m -> height dl3 = m -> 
  width dl1 n -> width dl2 n -> width dl3 n-> 
  mat_each' A sub ( mat_each' A sub dl1 dl2 ) dl3 
  = mat_each' A sub dl1 (mat_each' A add dl2 dl3).
Proof.
  induction m.
  induction n.
  induction dl1.
  - simpl. auto.
  - induction dl2.
    + simpl. auto.
    + induction dl3.
      { simpl. auto. }
      { simpl. intros. inversion H0. }
  - induction dl1.
    + simpl. auto.
    + induction dl2.
      { simpl. auto. }
      { induction dl3. 
        { simpl. auto. }
        { intros. inversion H0. } }
  - induction n. induction dl1.
    + simpl. auto.
    + induction dl2.
      { simpl. auto. }
      { induction dl3.
        { simpl. auto. }
        { simpl. intros. f_equal. apply list_sub_assoc. auto.
          apply IHm with (n:= 0). apply H. auto. auto. auto. inversion H3.
          auto. inversion H4. auto. inversion H5. auto. }}
   + induction dl1.
    { simpl. auto. }
    { induction dl2. 
      { simpl. auto. }
      { induction dl3.
        { simpl. auto. }
        { simpl. intros. f_equal. apply list_sub_assoc. auto. 
          apply IHm with (n:=S n). apply H.
           auto. auto. auto. inversion H3. auto. inversion H4.
           auto. inversion H5. auto. }} }
Qed.

(** ** matrix_sub_assoc *)
(** The associative law of the substraction of matrices :
    M1-M2-M3 = M1-(M2+M3). *)
Lemma matrix_sub_assoc : forall {m n:nat} (mat1 mat2 mat3 :@Mat A m n ) ,
   (forall a b c , sub (sub a b) c = sub a (add b c)) ->
   matrix_each A sub ( matrix_each A sub mat1 mat2 ) mat3 ===
   matrix_each A sub mat1 (matrix_each A add mat2 mat3).
Proof.
  intros.
  induction mat1.
  induction mat2.
  induction mat3.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_sub_assoc with (m:= m) (n:=n). apply H. apply mat_height.
  apply mat_height0. apply mat_height1. apply mat_width. apply mat_width0.
  apply mat_width1.
Qed.

(** * Substraction of Zero Matrix *)

(** *** list_sub_zero_l *)
(** The substraction of list l and zero list : lzero - l = - l. *)
Lemma list_sub_zero_l : forall (n:nat) l ,
 ((forall a , sub Zero a = negative a))->length l = n -> 
  list_each A sub (list_o A Zero n) l = list_map A negative l.
Proof.
  induction n. induction l.
  - simpl. intros. auto.
  - simpl. intros. inversion H0.
  - intros. simpl. induction l. auto. simpl. rewrite H. rewrite IHn;auto.
Qed.

(** *** dlist_sub_zero_l *)
(** The substraction of two-dimensional list dl and zero two-dimensional
    list : dlzero - dl = - dl. *)
Lemma dlist_sub_zero_l : forall m n ma , 
  (forall a , sub Zero a = negative a) -> 
  height ma = m -> width ma n -> 
  mat_each' A sub (dlist_o A Zero m n) ma = dlist_map A negative ma.
Proof.
  induction m.
  induction n.
  - simpl. intros. induction ma. auto. inversion H0.
  - simpl. intros. induction ma. auto. inversion H0.
  - induction n. induction ma.
    + simpl. auto.
    + simpl. intros. assert (a=nil). induction a. auto. 
      inversion H1. inversion H2. rewrite H2. rewrite IHm.
      auto. auto. auto. apply H1.
    + induction ma.
      { simpl. auto. }
      { intros. simpl. induction a. inversion H1. inversion H2.
        f_equal. simpl. rewrite H. f_equal.
        rewrite list_sub_zero_l.
        auto. apply H. inversion H1. inversion H2. auto. apply IHm;auto.
        inversion H1. apply H3. }
Qed.

(** ** matrix_sub_zero_l *)
(** The substraction of matrix M and zero matrix : MO - M = - M. *)
Lemma matrix_sub_zero_l : forall {m n:nat} {ma:@Mat A m n} ,
  (forall a , sub Zero a = negative a)-> 
    (matrix_each A sub (MO A Zero m n) ma) 
    === (matrix_map A negative ma).
Proof.
  intros m n.
  induction ma.
  intros.
  unfold matrix_each.
  unfold matrix_map.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_sub_zero_l;auto.
Qed.


(** * Matrix Substraction Associative Law *)

(** *** list_sub_zero_r *)
(** The substraction of list l and zero list : l - lzero = l. *)
Lemma list_sub_zero_r : forall (n:nat) (l:list A) ,
 ((forall a , sub a Zero = a))->length l = n -> 
  list_each A sub l (list_o A Zero n) = l.
Proof.
  induction n. induction l.
  - simpl. intros. auto.
  - simpl. intros. inversion H0.
  - intros. simpl. induction l. auto. simpl. rewrite H. rewrite IHn;auto.
Qed.

(** *** dlist_sub_zero_l *)
(** The substraction of two-dimensional list dl and zero two-dimensional
    list : dl - dlzero = dl. *)
Lemma dlist_sub_zero_r : forall m n ma , 
  (forall a , sub a Zero = a) -> 
  height ma = m -> width ma n -> 
  mat_each' A sub ma (dlist_o A Zero m n) = ma.
Proof.
  induction m.
  induction n.
  - simpl. intros. induction ma. auto. inversion H0.
  - simpl. intros. induction ma. auto. inversion H0.
  - induction n. induction ma.
    + simpl. auto.
    + simpl. intros. assert (a=nil). induction a. auto. 
      inversion H1. inversion H2. rewrite H2. rewrite IHm.
      auto. auto. auto. apply H1.
    + induction ma.
      { simpl. auto. }
      { intros. simpl. induction a. inversion H1. inversion H2.
        f_equal. simpl. rewrite H. rewrite list_sub_zero_r;auto. 
        inversion H1. inversion H2. auto. apply IHm;auto.
        inversion H1. apply H3. }
Qed.

(** ** matrix_sub_zero_l *)
(** The substraction of matrix M and zero matrix : M - MO = M. *)
Lemma matrix_sub_zero_r : forall {m n:nat} (ma:@Mat A m n ) ,
  (forall a , sub a Zero = a)-> 
  matrix_each A sub ma (MO A Zero m n) === ma.
Proof.
  intros m n.
  induction ma.
  intros.
  unfold matrix_each.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_sub_zero_r;auto.
Qed.

(** * Substraction of Matrix itself *)

(** *** list_sub_self *)
(** The substraction of list l and it self : l - l = lzero *)
Lemma list_sub_self : forall (n:nat) (l:list A) ,
 ((forall a , sub a a = Zero))->length l = n -> 
  list_each A sub l l = (list_o A Zero n).
Proof.
  induction n. induction l.
  - simpl. intros. auto.
  - simpl. intros. inversion H0.
  - intros. simpl. induction l. simpl in H0. discriminate H0. 
    simpl. rewrite H. rewrite IHn;auto.
Qed.

(** *** dlist_sub_self *)
(** The substraction of two dimensional list dl and itself :
    dl - dl = dlzero *)
Lemma dlist_sub_self : forall(m n:nat) (ma:list (list A)) , 
  (forall a , sub a a = Zero) -> 
  height ma = m -> width ma n -> 
  mat_each' A sub ma ma = (dlist_o A Zero m n).
Proof.
  induction m.
  induction n.
  - simpl. intros. induction ma. auto. inversion H0.
  - simpl. intros. induction ma. auto. inversion H0.
  - induction n. induction ma.
    + simpl. intros. discriminate H0.
    + simpl. intros. assert (a=nil). induction a. auto. 
      inversion H1. inversion H2. rewrite H2. simpl. f_equal. apply IHm.
      assumption. inversion H0. auto. destruct H1. assumption. 
    + induction ma.
      { simpl. auto. intros. discriminate H0. }
      { intros. simpl. induction a. inversion H1. inversion H2.
        f_equal. simpl. rewrite H. f_equal. apply list_sub_self.
        assumption. inversion H1. inversion H2. auto.
         apply IHm;auto.
        inversion H1. apply H3. }
Qed.

(** ** matrix_sub_self *)
(** The substraction of matrix M and it self. *)
Lemma matrix_sub_self : forall {m n:nat} (ma:@Mat A m n) ,
  (forall a , sub a a = Zero)-> 
  matrix_each A sub ma ma === MO A Zero m n.
Proof.
  intros m n.
  induction ma.
  intros.
  unfold matrix_each.
  unfold M_eq.
  simpl.
  unfold mat_each.
  simpl.
  apply dlist_sub_self. auto.
  assumption. assumption.
Qed.


End sub_lemma.
